package stp.examples;

import junit.framework.TestCase;
import stp.*;

public class b5 extends TestCase{
public void test() {
System.out.printf("x,y,lambda,_x,_y,_lambda:BITVECTOR(8);\n");
System.out.printf("at,_at:BITVECTOR(4);\n");
VC vc = new VC();
//vc.setFlags('w');
//vc.setFlags('r');
vc.push();
Expr e19223 = vc.varExpr( "at", vc.bvType( 4));
Expr e19224 = vc.bvConstExprFromStr( "1000");
Expr e19225 = vc.eqExpr( e19223, e19224);
Expr e19226 = vc.varExpr( "x", vc.bvType( 8));
Expr e19227 = vc.bvConstExprFromStr( "00000001");
Expr e19228 = vc.sbvGtExpr( e19226, e19227);
Expr e19229 = vc.andExpr( e19225, e19228);
Expr e19230 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19231 = vc.varExpr( "x", vc.bvType( 8));
Expr e19232 = vc.iteExpr( vc.bvBoolExtract( e19230, 0), vc.bvRightShiftExpr( 1 << 0, e19231), e19231);
Expr e19233 = vc.iteExpr( vc.bvBoolExtract( e19230, 1), vc.bvRightShiftExpr( 1 << 1, e19232), e19232);
Expr e19234 = vc.iteExpr( vc.bvBoolExtract( e19230, 2), vc.bvRightShiftExpr( 1 << 2, e19233), e19233);
Expr e19235 = vc.iteExpr( vc.sbvGeExpr( e19230, vc.bvConstExprFromInt(8,8)), vc.bvConstExprFromInt( 8, 0), e19234);
Expr e19236 = vc.bvConstExprFromStr( "00000001");
Expr e19237 = vc.eqExpr( e19235, e19236);
Expr e19238 = vc.impliesExpr( e19229, e19237);
Expr e19239 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19240 = vc.eqExpr( vc.bvExtract( e19239, 2, 2), vc.bvConstExprFromStr( "1"));
Expr e19241 = vc.notExpr( e19240);
Expr e19242 = vc.varExpr( "y", vc.bvType( 8));
Expr e19243 = vc.eqExpr( vc.bvExtract( e19242, 7, 7), vc.bvConstExprFromStr( "1"));
Expr e19244 = vc.notExpr( e19243);
Expr e19245 = vc.orExpr( e19241, e19244);
Expr e19246 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19247 = vc.eqExpr( vc.bvExtract( e19246, 6, 6), vc.bvConstExprFromStr( "1"));
Expr e19248 = vc.notExpr( e19247);
Expr e19249 = vc.varExpr( "y", vc.bvType( 8));
Expr e19250 = vc.eqExpr( vc.bvExtract( e19249, 7, 7), vc.bvConstExprFromStr( "1"));
Expr e19251 = vc.notExpr( e19250);
Expr e19252 = vc.orExpr( e19248, e19251);
Expr e19253 = vc.andExpr( e19245, e19252);
Expr e19254 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19255 = vc.eqExpr( vc.bvExtract( e19254, 0, 0), vc.bvConstExprFromStr( "1"));
Expr e19256 = vc.notExpr( e19255);
Expr e19257 = vc.varExpr( "at", vc.bvType( 4));
Expr e19258 = vc.eqExpr( vc.bvExtract( e19257, 3, 3), vc.bvConstExprFromStr( "1"));
Expr e19259 = vc.orExpr( e19256, e19258);
Expr e19260 = vc.andExpr( e19253, e19259);
Expr e19261 = vc.varExpr( "y", vc.bvType( 8));
Expr e19262 = vc.bvConstExprFromStr( "00000010");
Expr e19263 = vc.eqExpr( e19261, e19262);
Expr e19264 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19265 = vc.bvConstExprFromStr( "01100100");
Expr e19266 = vc.eqExpr( e19264, e19265);
Expr e19267 = vc.andExpr( e19263, e19266);
Expr e19268 = vc.varExpr( "x", vc.bvType( 8));
Expr e19269 = vc.bvConstExprFromStr( "00110100");
Expr e19270 = vc.eqExpr( e19268, e19269);
Expr e19271 = vc.andExpr( e19267, e19270);
Expr e19272 = vc.varExpr( "at", vc.bvType( 4));
Expr e19273 = vc.bvConstExprFromStr( "0100");
Expr e19274 = vc.eqExpr( e19272, e19273);
Expr e19275 = vc.andExpr( e19271, e19274);
Expr e19276 = vc.notExpr( e19275);
Expr e19277 = vc.andExpr( e19260, e19276);
Expr e19278 = vc.andExpr( e19238, e19277);
Expr e19279 = vc.varExpr( "at", vc.bvType( 4));
Expr e19280 = vc.bvConstExprFromStr( "0001");
Expr e19281 = vc.eqExpr( e19279, e19280);
Expr e19282 = vc.varExpr( "y", vc.bvType( 8));
Expr e19283 = vc.bvConstExprFromStr( "11110000");
Expr e19284 = vc.bvAndExpr( e19282, e19283);
Expr e19285 = vc.bvConstExprFromStr( "00000000");
Expr e19286 = vc.eqExpr( e19284, e19285);
Expr e19287 = vc.notExpr( e19286);
Expr e19288 = vc.andExpr( e19281, e19287);
Expr e19289 = vc.varExpr( "_at", vc.bvType( 4));
Expr e19290 = vc.bvConstExprFromStr( "0010");
Expr e19291 = vc.eqExpr( e19289, e19290);
Expr e19292 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19293 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19294 = vc.bvConstExprFromStr( "00000100");
Expr e19295 = vc.bvPlusExpr( 8, e19293, e19294);
Expr e19296 = vc.eqExpr( e19292, e19295);
Expr e19297 = vc.andExpr( e19291, e19296);
Expr e19298 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19299 = vc.varExpr( "y", vc.bvType( 8));
Expr e19300 = vc.bvRightShiftExpr( 4, e19299);
Expr e19301 = vc.eqExpr( e19298, e19300);
Expr e19302 = vc.andExpr( e19297, e19301);
Expr e19303 = vc.varExpr( "_x", vc.bvType( 8));
Expr e19304 = vc.varExpr( "x", vc.bvType( 8));
Expr e19305 = vc.eqExpr( e19303, e19304);
Expr e19306 = vc.andExpr( e19302, e19305);
Expr e19307 = vc.andExpr( e19288, e19306);
Expr e19308 = vc.varExpr( "at", vc.bvType( 4));
Expr e19309 = vc.bvConstExprFromStr( "0001");
Expr e19310 = vc.eqExpr( e19308, e19309);
Expr e19311 = vc.varExpr( "y", vc.bvType( 8));
Expr e19312 = vc.bvConstExprFromStr( "11110000");
Expr e19313 = vc.bvAndExpr( e19311, e19312);
Expr e19314 = vc.bvConstExprFromStr( "00000000");
Expr e19315 = vc.eqExpr( e19313, e19314);
Expr e19316 = vc.andExpr( e19310, e19315);
Expr e19317 = vc.varExpr( "_at", vc.bvType( 4));
Expr e19318 = vc.bvConstExprFromStr( "0010");
Expr e19319 = vc.eqExpr( e19317, e19318);
Expr e19320 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19321 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19322 = vc.eqExpr( e19320, e19321);
Expr e19323 = vc.andExpr( e19319, e19322);
Expr e19324 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19325 = vc.varExpr( "y", vc.bvType( 8));
Expr e19326 = vc.eqExpr( e19324, e19325);
Expr e19327 = vc.andExpr( e19323, e19326);
Expr e19328 = vc.varExpr( "_x", vc.bvType( 8));
Expr e19329 = vc.varExpr( "x", vc.bvType( 8));
Expr e19330 = vc.eqExpr( e19328, e19329);
Expr e19331 = vc.andExpr( e19327, e19330);
Expr e19332 = vc.andExpr( e19316, e19331);
Expr e19333 = vc.orExpr( e19307, e19332);
Expr e19334 = vc.varExpr( "at", vc.bvType( 4));
Expr e19335 = vc.bvConstExprFromStr( "0010");
Expr e19336 = vc.eqExpr( e19334, e19335);
Expr e19337 = vc.varExpr( "y", vc.bvType( 8));
Expr e19338 = vc.bvConstExprFromStr( "11001100");
Expr e19339 = vc.bvAndExpr( e19337, e19338);
Expr e19340 = vc.bvConstExprFromStr( "00000000");
Expr e19341 = vc.eqExpr( e19339, e19340);
Expr e19342 = vc.notExpr( e19341);
Expr e19343 = vc.andExpr( e19336, e19342);
Expr e19344 = vc.varExpr( "_at", vc.bvType( 4));
Expr e19345 = vc.bvConstExprFromStr( "0100");
Expr e19346 = vc.eqExpr( e19344, e19345);
Expr e19347 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19348 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19349 = vc.bvConstExprFromStr( "00000010");
Expr e19350 = vc.bvPlusExpr( 8, e19348, e19349);
Expr e19351 = vc.eqExpr( e19347, e19350);
Expr e19352 = vc.andExpr( e19346, e19351);
Expr e19353 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19354 = vc.varExpr( "y", vc.bvType( 8));
Expr e19355 = vc.bvRightShiftExpr( 2, e19354);
Expr e19356 = vc.eqExpr( e19353, e19355);
Expr e19357 = vc.andExpr( e19352, e19356);
Expr e19358 = vc.varExpr( "_x", vc.bvType( 8));
Expr e19359 = vc.varExpr( "x", vc.bvType( 8));
Expr e19360 = vc.eqExpr( e19358, e19359);
Expr e19361 = vc.andExpr( e19357, e19360);
Expr e19362 = vc.andExpr( e19343, e19361);
Expr e19363 = vc.orExpr( e19333, e19362);
Expr e19364 = vc.varExpr( "at", vc.bvType( 4));
Expr e19365 = vc.bvConstExprFromStr( "0010");
Expr e19366 = vc.eqExpr( e19364, e19365);
Expr e19367 = vc.varExpr( "y", vc.bvType( 8));
Expr e19368 = vc.bvConstExprFromStr( "11001100");
Expr e19369 = vc.bvAndExpr( e19367, e19368);
Expr e19370 = vc.bvConstExprFromStr( "00000000");
Expr e19371 = vc.eqExpr( e19369, e19370);
Expr e19372 = vc.andExpr( e19366, e19371);
Expr e19373 = vc.varExpr( "_at", vc.bvType( 4));
Expr e19374 = vc.bvConstExprFromStr( "0100");
Expr e19375 = vc.eqExpr( e19373, e19374);
Expr e19376 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19377 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19378 = vc.eqExpr( e19376, e19377);
Expr e19379 = vc.andExpr( e19375, e19378);
Expr e19380 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19381 = vc.varExpr( "y", vc.bvType( 8));
Expr e19382 = vc.eqExpr( e19380, e19381);
Expr e19383 = vc.andExpr( e19379, e19382);
Expr e19384 = vc.varExpr( "_x", vc.bvType( 8));
Expr e19385 = vc.varExpr( "x", vc.bvType( 8));
Expr e19386 = vc.eqExpr( e19384, e19385);
Expr e19387 = vc.andExpr( e19383, e19386);
Expr e19388 = vc.andExpr( e19372, e19387);
Expr e19389 = vc.orExpr( e19363, e19388);
Expr e19390 = vc.varExpr( "at", vc.bvType( 4));
Expr e19391 = vc.bvConstExprFromStr( "0100");
Expr e19392 = vc.eqExpr( e19390, e19391);
Expr e19393 = vc.varExpr( "y", vc.bvType( 8));
Expr e19394 = vc.bvConstExprFromStr( "10101010");
Expr e19395 = vc.bvAndExpr( e19393, e19394);
Expr e19396 = vc.bvConstExprFromStr( "00000000");
Expr e19397 = vc.eqExpr( e19395, e19396);
Expr e19398 = vc.notExpr( e19397);
Expr e19399 = vc.andExpr( e19392, e19398);
Expr e19400 = vc.varExpr( "_at", vc.bvType( 4));
Expr e19401 = vc.bvConstExprFromStr( "1000");
Expr e19402 = vc.eqExpr( e19400, e19401);
Expr e19403 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19404 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19405 = vc.bvConstExprFromStr( "00000001");
Expr e19406 = vc.bvPlusExpr( 8, e19404, e19405);
Expr e19407 = vc.eqExpr( e19403, e19406);
Expr e19408 = vc.andExpr( e19402, e19407);
Expr e19409 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19410 = vc.varExpr( "y", vc.bvType( 8));
Expr e19411 = vc.bvRightShiftExpr( 1, e19410);
Expr e19412 = vc.eqExpr( e19409, e19411);
Expr e19413 = vc.andExpr( e19408, e19412);
Expr e19414 = vc.varExpr( "_x", vc.bvType( 8));
Expr e19415 = vc.varExpr( "x", vc.bvType( 8));
Expr e19416 = vc.eqExpr( e19414, e19415);
Expr e19417 = vc.andExpr( e19413, e19416);
Expr e19418 = vc.andExpr( e19399, e19417);
Expr e19419 = vc.orExpr( e19389, e19418);
Expr e19420 = vc.varExpr( "at", vc.bvType( 4));
Expr e19421 = vc.bvConstExprFromStr( "0100");
Expr e19422 = vc.eqExpr( e19420, e19421);
Expr e19423 = vc.varExpr( "y", vc.bvType( 8));
Expr e19424 = vc.bvConstExprFromStr( "10101010");
Expr e19425 = vc.bvAndExpr( e19423, e19424);
Expr e19426 = vc.bvConstExprFromStr( "00000000");
Expr e19427 = vc.eqExpr( e19425, e19426);
Expr e19428 = vc.andExpr( e19422, e19427);
Expr e19429 = vc.varExpr( "_at", vc.bvType( 4));
Expr e19430 = vc.bvConstExprFromStr( "1000");
Expr e19431 = vc.eqExpr( e19429, e19430);
Expr e19432 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19433 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19434 = vc.eqExpr( e19432, e19433);
Expr e19435 = vc.andExpr( e19431, e19434);
Expr e19436 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19437 = vc.varExpr( "y", vc.bvType( 8));
Expr e19438 = vc.eqExpr( e19436, e19437);
Expr e19439 = vc.andExpr( e19435, e19438);
Expr e19440 = vc.varExpr( "_x", vc.bvType( 8));
Expr e19441 = vc.varExpr( "x", vc.bvType( 8));
Expr e19442 = vc.eqExpr( e19440, e19441);
Expr e19443 = vc.andExpr( e19439, e19442);
Expr e19444 = vc.andExpr( e19428, e19443);
Expr e19445 = vc.orExpr( e19419, e19444);
Expr e19446 = vc.varExpr( "at", vc.bvType( 4));
Expr e19447 = vc.bvConstExprFromStr( "1000");
Expr e19448 = vc.eqExpr( e19446, e19447);
Expr e19449 = vc.varExpr( "_at", vc.bvType( 4));
Expr e19450 = vc.varExpr( "at", vc.bvType( 4));
Expr e19451 = vc.eqExpr( e19449, e19450);
Expr e19452 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19453 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19454 = vc.eqExpr( e19452, e19453);
Expr e19455 = vc.andExpr( e19451, e19454);
Expr e19456 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19457 = vc.varExpr( "y", vc.bvType( 8));
Expr e19458 = vc.eqExpr( e19456, e19457);
Expr e19459 = vc.andExpr( e19455, e19458);
Expr e19460 = vc.varExpr( "_x", vc.bvType( 8));
Expr e19461 = vc.varExpr( "x", vc.bvType( 8));
Expr e19462 = vc.eqExpr( e19460, e19461);
Expr e19463 = vc.andExpr( e19459, e19462);
Expr e19464 = vc.andExpr( e19448, e19463);
Expr e19465 = vc.orExpr( e19445, e19464);
Expr e19466 = vc.andExpr( e19278, e19465);
Expr e19467 = vc.varExpr( "lambda", vc.bvType( 8));
Expr e19468 = vc.eqExpr( vc.bvExtract( e19467, 6, 6), vc.bvConstExprFromStr( "1"));
Expr e19469 = vc.notExpr( e19468);
Expr e19470 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19471 = vc.eqExpr( vc.bvExtract( e19470, 6, 6), vc.bvConstExprFromStr( "1"));
Expr e19472 = vc.notExpr( e19471);
Expr e19473 = vc.notExpr( e19472);
Expr e19474 = vc.andExpr( e19469, e19473);
Expr e19475 = vc.andExpr( e19466, e19474);
vc.assertFormula( e19475);
vc.printAsserts(false);
Expr e19476 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19477 = vc.eqExpr( vc.bvExtract( e19476, 3, 3), vc.bvConstExprFromStr( "1"));
Expr e19478 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19479 = vc.eqExpr( vc.bvExtract( e19478, 4, 4), vc.bvConstExprFromStr( "1"));
Expr e19480 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19481 = vc.eqExpr( vc.bvExtract( e19480, 5, 5), vc.bvConstExprFromStr( "1"));
Expr e19482 = vc.notExpr( e19481);
Expr e19483 = vc.varExpr( "_lambda", vc.bvType( 8));
Expr e19484 = vc.eqExpr( vc.bvExtract( e19483, 7, 7), vc.bvConstExprFromStr( "1"));
Expr e19485 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19486 = vc.eqExpr( vc.bvExtract( e19485, 0, 0), vc.bvConstExprFromStr( "1"));
Expr e19487 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19488 = vc.eqExpr( vc.bvExtract( e19487, 1, 1), vc.bvConstExprFromStr( "1"));
Expr e19489 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19490 = vc.eqExpr( vc.bvExtract( e19489, 2, 2), vc.bvConstExprFromStr( "1"));
Expr e19491 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19492 = vc.eqExpr( vc.bvExtract( e19491, 3, 3), vc.bvConstExprFromStr( "1"));
Expr e19493 = vc.notExpr( e19492);
Expr e19494 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19495 = vc.eqExpr( vc.bvExtract( e19494, 4, 4), vc.bvConstExprFromStr( "1"));
Expr e19496 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19497 = vc.eqExpr( vc.bvExtract( e19496, 5, 5), vc.bvConstExprFromStr( "1"));
Expr e19498 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19499 = vc.eqExpr( vc.bvExtract( e19498, 6, 6), vc.bvConstExprFromStr( "1"));
Expr e19500 = vc.varExpr( "_y", vc.bvType( 8));
Expr e19501 = vc.eqExpr( vc.bvExtract( e19500, 7, 7), vc.bvConstExprFromStr( "1"));
Expr e19502 = vc.orExpr( e19499, e19501);
Expr e19503 = vc.orExpr( e19497, e19502);
Expr e19504 = vc.orExpr( e19495, e19503);
Expr e19505 = vc.orExpr( e19493, e19504);
Expr e19506 = vc.orExpr( e19490, e19505);
Expr e19507 = vc.orExpr( e19488, e19506);
Expr e19508 = vc.orExpr( e19486, e19507);
Expr e19509 = vc.orExpr( e19484, e19508);
Expr e19510 = vc.orExpr( e19482, e19509);
Expr e19511 = vc.orExpr( e19479, e19510);
Expr e19512 = vc.orExpr( e19477, e19511);
vc.push();
System.out.printf("QUERY(");
vc.printExpr( e19512);
System.out.printf(");\n");
vc.query( e19512);
}
}
